1. Technical Field
The present invention relates to computer verification and more particularly to systems and methods for reducing warnings by employing synchronization constraints, sound invariants and model checking.
2. Description of the Related Art
Concrete error traces are critical for debugging software. Unfortunately, generating error traces for concurrency related bugs is notoriously hard. One of the key reasons for this is that concurrent programs are behaviorally complex involving subtle interactions between threads which makes them difficult to analyze. This complex behavior is the result of the many possible interleavings among the local operations of the various threads comprising a given concurrent program.
The development of debugging techniques for concurrent programs is currently an area of active research due to the on-going multi-core revolution. Testing, static analysis and model checking have all been explored but not without drawbacks. Testing has clearly been the most effective debugging technique for sequential programs. However, the key challenge for applying testing to concurrent programs is due the many possible interleavings among threads so that it is difficult to provide meaningful coverage metrics. Furthermore, more often than not, concurrent systems have in-built non-determinism because of which replayability is difficult to guarantee, i.e., the same input may yield different results in different runs of the concurrent program.
The use of static analysis has found some degree of success for standard concurrency bugs like data races and deadlocks. A data race occurs when two different threads in a given program can both simultaneously access a shared variable, with at least one of the accesses being a write operation. Checking for data races is often a critical first step in the debugging of concurrent programs. Indeed, the presence of data races in a program typically renders its behavior non-deterministic thereby making it difficult to reason about it for more complex and interesting properties.
The main drawback of static analysis, however, is that a large number of bogus warnings can often be generated which do not correspond to true bugs. This places the burden of sifting the true bugs from the false warnings on the programmer. From a programmer's perspective, this is clearly undesirable. If the bogus warning rate exceeds a certain threshold programmers may simply abandon the use of such techniques.
Model checking has the advantage that it produces only concrete error traces and thus does not rely on the programmer to inspect the warnings and decide whether they are true bugs. However, the state explosion problem severely limits its scalability. It is unrealistic to expect model checking to scale to large real-life concurrent programs.